Problem:
0(q0(0(x1))) -> 0(0(q0(x1)))
0(q0(h(x1))) -> 0(0(q0(h(x1))))
0(q0(1(x1))) -> 0(1(q0(x1)))
1(q0(0(x1))) -> 0(0(q1(x1)))
1(q0(h(x1))) -> 0(0(q1(h(x1))))
1(q0(1(x1))) -> 0(1(q1(x1)))
1(q1(0(x1))) -> 1(0(q1(x1)))
1(q1(h(x1))) -> 1(0(q1(h(x1))))
1(q1(1(x1))) -> 1(1(q1(x1)))
0(q1(0(x1))) -> 0(0(q2(x1)))
0(q1(h(x1))) -> 0(0(q2(h(x1))))
0(q1(1(x1))) -> 0(1(q2(x1)))
1(q2(0(x1))) -> 1(0(q2(x1)))
1(q2(h(x1))) -> 1(0(q2(h(x1))))
1(q2(1(x1))) -> 1(1(q2(x1)))
0(q2(x1)) -> q3(1(x1))
1(q3(x1)) -> q3(1(x1))
0(q3(x1)) -> q4(0(x1))
1(q4(x1)) -> q4(1(x1))
0(q4(0(x1))) -> 1(0(q5(x1)))
0(q4(h(x1))) -> 1(0(q5(h(x1))))
0(q4(1(x1))) -> 1(1(q5(x1)))
1(q5(0(x1))) -> 0(0(q1(x1)))
1(q5(h(x1))) -> 0(0(q1(h(x1))))
1(q5(1(x1))) -> 0(1(q1(x1)))
h(q0(x1)) -> h(0(q0(x1)))
h(q1(x1)) -> h(0(q1(x1)))
h(q2(x1)) -> h(0(q2(x1)))
h(q3(x1)) -> h(0(q3(x1)))
h(q4(x1)) -> h(0(q4(x1)))
h(q5(x1)) -> h(0(q5(x1)))
Proof:
Bounds Processor:
bound: 4
enrichment: match
automaton:
final states: {9,8,7}
transitions:
h3(345) -> 346*
h1(72) -> 73*
q52(334) -> 335*
q52(336) -> 337*
q52(326) -> 327*
q52(316) -> 317*
q52(328) -> 329*
q52(342) -> 343*
01(60) -> 61*
01(52) -> 53*
01(54) -> 55*
01(44) -> 45*
01(71) -> 72*
01(46) -> 47*
01(36) -> 37*
14(356) -> 357*
q51(202) -> 203*
q51(192) -> 193*
q51(194) -> 195*
q51(208) -> 209*
q51(210) -> 211*
q51(200) -> 201*
04(355) -> 356*
q41(62) -> 63*
q41(37) -> 38*
q41(184) -> 185*
q41(186) -> 187*
q41(176) -> 177*
q41(178) -> 179*
q41(168) -> 169*
q41(170) -> 171*
q54(354) -> 355*
q31(162) -> 163*
q31(152) -> 153*
q31(154) -> 155*
q31(144) -> 145*
q31(14) -> 15*
q31(146) -> 147*
q31(160) -> 161*
q13(366) -> 367*
q21(122) -> 123*
q21(136) -> 137*
q21(138) -> 139*
q21(128) -> 129*
q21(130) -> 131*
q21(120) -> 121*
q11(112) -> 113*
q11(114) -> 115*
q11(104) -> 105*
q11(106) -> 107*
q11(96) -> 97*
q11(98) -> 99*
q01(90) -> 91*
q01(80) -> 81*
q01(70) -> 71*
q01(82) -> 83*
q01(74) -> 75*
q01(88) -> 89*
11(30) -> 31*
11(32) -> 33*
11(22) -> 23*
11(24) -> 25*
11(16) -> 17*
11(13) -> 14*
q42(314) -> 315*
q42(246) -> 247*
00(5) -> 7*
00(2) -> 7*
00(4) -> 7*
00(6) -> 7*
00(1) -> 7*
00(3) -> 7*
02(272) -> 273*
02(262) -> 263*
02(264) -> 265*
02(254) -> 255*
02(266) -> 267*
02(256) -> 257*
02(313) -> 314*
02(248) -> 249*
02(245) -> 246*
q00(5) -> 1*
q00(2) -> 1*
q00(4) -> 1*
q00(6) -> 1*
q00(1) -> 1*
q00(3) -> 1*
q32(215) -> 216*
h0(5) -> 9*
h0(2) -> 9*
h0(4) -> 9*
h0(6) -> 9*
h0(1) -> 9*
h0(3) -> 9*
12(232) -> 233*
12(222) -> 223*
12(224) -> 225*
12(214) -> 215*
12(318) -> 319*
12(238) -> 239*
12(230) -> 231*
12(317) -> 318*
10(5) -> 8*
10(2) -> 8*
10(4) -> 8*
10(6) -> 8*
10(1) -> 8*
10(3) -> 8*
h2(267) -> 268*
q10(5) -> 2*
q10(2) -> 2*
q10(4) -> 2*
q10(6) -> 2*
q10(1) -> 2*
q10(3) -> 2*
13(364) -> 365*
13(284) -> 285*
13(363) -> 364*
13(367) -> 368*
q20(5) -> 3*
q20(2) -> 3*
q20(4) -> 3*
q20(6) -> 3*
q20(1) -> 3*
q20(3) -> 3*
03(344) -> 345*
03(279) -> 280*
03(368) -> 369*
03(283) -> 284*
q30(5) -> 4*
q30(2) -> 4*
q30(4) -> 4*
q30(6) -> 4*
q30(1) -> 4*
q30(3) -> 4*
q53(302) -> 303*
q53(292) -> 293*
q53(282) -> 283*
q53(294) -> 295*
q53(308) -> 309*
q53(300) -> 301*
q53(362) -> 363*
q40(5) -> 5*
q40(2) -> 5*
q40(4) -> 5*
q40(6) -> 5*
q40(1) -> 5*
q40(3) -> 5*
q43(280) -> 281*
q50(5) -> 6*
q50(2) -> 6*
q50(4) -> 6*
q50(6) -> 6*
q50(1) -> 6*
q50(3) -> 6*
1 -> 208,184,160,136,112,88,54,30
2 -> 194,170,146,122,98,74,44,16
3 -> 210,186,162,138,114,90,60,32
4 -> 200,176,152,128,104,80,46,22
5 -> 192,168,144,120,96,70,36,13
6 -> 202,178,154,130,106,82,52,24
13 -> 342*
14 -> 313,62
15 -> 231,215,246,23,14,62,61,37,8,7
16 -> 336*
17 -> 14*
22 -> 328*
23 -> 14*
24 -> 334*
25 -> 14*
30 -> 316*
31 -> 14*
32 -> 326*
33 -> 14*
38 -> 249,246,47,7
45 -> 37*
47 -> 37*
53 -> 37*
55 -> 37*
61 -> 37*
63 -> 239,215,14,62,8
73 -> 9*
75 -> 71*
81 -> 71*
83 -> 71*
89 -> 71*
91 -> 71*
97 -> 71*
99 -> 71*
105 -> 71*
107 -> 71*
113 -> 71*
115 -> 71*
120 -> 238*
121 -> 71*
122 -> 214*
123 -> 71*
128 -> 230*
129 -> 71*
130 -> 232*
131 -> 71*
136 -> 222*
137 -> 71*
138 -> 224*
139 -> 71*
144 -> 256*
145 -> 71*
146 -> 262*
147 -> 71*
152 -> 248*
153 -> 71*
154 -> 254*
155 -> 71*
160 -> 264*
161 -> 71*
162 -> 245*
163 -> 71*
169 -> 71*
171 -> 71*
177 -> 71*
179 -> 71*
185 -> 71*
187 -> 71*
193 -> 71*
195 -> 71*
201 -> 71*
203 -> 71*
209 -> 71*
211 -> 71*
215 -> 279*
216 -> 266,72
223 -> 215*
225 -> 215*
231 -> 215*
233 -> 215*
239 -> 215*
245 -> 308*
247 -> 272,72
248 -> 302*
249 -> 246*
254 -> 294*
255 -> 246*
256 -> 300*
257 -> 246*
262 -> 282*
263 -> 246*
264 -> 292*
265 -> 246*
268 -> 73,9
273 -> 267*
279 -> 354*
281 -> 344,267
285 -> 273,267
293 -> 283*
295 -> 283*
301 -> 283*
303 -> 283*
309 -> 283*
315 -> 314,280
317 -> 366*
318 -> 362*
319 -> 314,280
327 -> 317*
329 -> 317*
335 -> 317*
337 -> 317*
343 -> 317*
346 -> 268,73
357 -> 345*
365 -> 345*
369 -> 364*
problem:
Qed